Add iommu support to microkit by Cheng-Li1 · Pull Request #467 · seL4/microkit

Cheng-Li1 · 2026-04-10T08:04:33Z

This pull request adds iommu support for Microkit and needs Rust-Sel4 with the iommu support to work.

Supported features:
Map the memory region to a device-visible memory address.

Tests done:
Blk example with iommu feature enabled on x86 qemu and hardware(vb-105).

dreamliner787-9 · 2026-04-16T01:36:59Z

+    sel4::Config,
+};
+
+// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level.


I forgot the content of the conversation we had offline about this. But what happens when the target machine only support 3 levels VT-d page table, but we made a 4 levels one (according to VTD_PAGE_TABLE_LEVEL)?

dreamliner787-9 · 2026-04-16T01:41:24Z

Your commit history needs to be cleaned up and squashed. Some of the commits checked in code that should not be in Microkit, then other commits removed them.

dreamliner787-9 · 2026-04-16T01:49:43Z

A nice to have would be a minimal example showing this in action on QEMU x86, like the arm_smc or x86_64_ioport examples, as a proof that it works.

For example, you can use QEMU's DMA-capable "educational device": https://www.qemu.org/docs/master/specs/edu.html. You copy some data from normal RAM into the device's SRAM with a DMA transaction, then read back the device's SRAM via normal MMIO to verify that the transfer succeeded.

midnightveil

Misc things.

I'm not quite sure how this is supposed to be used in the SDF file.

I can only vaguely infer from the error tests you added, but you should add documentation on how to use this and what that means for the layout of the page tables for both.

midnightveil · 2026-04-16T07:26:18Z

 use sel4_capdl_initializer_types::{
-    object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec,
-    Word,
+    object::{self},


Why object::{self}. What was wrong with just object?

midnightveil · 2026-04-16T07:26:59Z

+    for frame_obj_id in frames.iter() {
+        // Make a cap for this frame.
+        let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, false, false);


Suggested change

for frame_obj_id in frames.iter() {

// Make a cap for this frame.

let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, false, false);

for &frame_obj_id in frames.iter() {

// Make a cap for this frame.

let frame_cap = capdl_util_make_frame_cap(frame_obj_id, read, write, /* what does this mean */ false, /* what does this mean */ false);

midnightveil · 2026-04-16T07:27:42Z

-        // Step 3-4 Create Scheduling Context
+        // Step 3-4 Create and Map IO Page Table Structure
+        if kernel_config.iommu {
+            let mut pci_to_iospace: HashMap<(u8, u8, u8), ObjectId> = HashMap::new();


This is assuming x86-specificness.

Do we not have a PciDev type anyway, that would make this nicer

also what happened to the domain id from the rust-seL4 pr?

midnightveil · 2026-04-16T07:29:45Z

+};
+
+// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level.
+// Sel4 will only attempt to use the four-level structure if the hardware does not supports three level.


seL4.
Check the grammar.

midnightveil · 2026-04-16T07:30:06Z

+
+// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level.
+// Sel4 will only attempt to use the four-level structure if the hardware does not supports three level.
+// https://github.com/seL4/seL4/blob/c406015c389decc4559fd44cb69604ddd24a0ddb/src/plat/pc99/machine/intel-vtd.c#L498


Use a link to a commit tag preferably over a random commit hash, e.g. seL4/seL4/blob/15.0.0.

Also, seL4 not Sel4

midnightveil · 2026-04-16T07:45:39Z

+    pub name: String,
+    pub pci_bus: u8,
+    pub pci_dev: u8,
+    pub dev_func: u8,
+    pub ioaddr: u64,
+    pub perms: u8,
+    pub text_pos: Option<roxmltree::TextPos>,


Same comments as the rust-seL4 PR: the PCI stuff should be part of x86 as itis arch-speicific.

midnightveil · 2026-04-16T07:46:13Z

+                if map_end > crate::capdl::iomem::VTD_MAX_ADDR {
+                    return Err(
+                        format!(
+                            "Error: iomap for '{}' has address 0x{:x} which exceeds the upper limits of {} in {} '{}' @ {}",


midnightveil · 2026-04-16T07:47:07Z

            },
            ObjectType::AsidPool => Some(object_sizes.asid_pool),
+            ObjectType::IOPageTable => Some(12),
+            // It would be best to avoid such catch all case so people might forget to add the size of new object type here.


Fix it or make an issue I think

midnightveil · 2026-04-16T07:47:17Z

@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW.


midnightveil · 2026-04-16T07:47:45Z

@@ -68,7 +68,7 @@
    "KernelPlatform": "pc99",
    "KernelX86MicroArch": "generic",
    # See https://github.com/seL4/microkit/issues/418 for details.


remove this comment if its solved

Cheng-Li1 · 2026-06-10T05:30:57Z

Things left to do:

Sort out the problem of the three-level vs four-level IO page table.
Implement the minimal IOMMU example.
Integrate with sdfgen.
Resolve other minor issues.

The issue behind the three-level vs four-level IO page table is that the IO page table level the seL4 will select for the board to use is only known at runtime. When generating the spec, the program has to assume a three-level or four-level IO page table structure, causing a potential mismatch. Currently, the program assumes a four-level IO page table structure, but only accepts memory regions that can fit into the three-level IO page table structure. At runtime, if the three-level IO page table is selected by seL4, the capdl initializer will skip mapping the root page table object, effectively treating the structure as a three-level IO page table. However, this approach will unnecessarily waste the memory because the root page table object is not mapped in. A better approach is to default the IO page table to three-level, but generate another page table object in the capdl initializer on demand. However, it might be tricky to implement due to how objects are generated in the capdl initializer.

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Perms and setvar are supported. Page size optimization logic has been refined. Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Fix the issue of duplicate objects names conflict when one pd owns multiple iospaces. Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>